//SIGNATURES

//classe Utente
abstract sig Utente{

	//ad ogni utente sono associati un username ed una password
	username: one Username,
	password: one Password,
	
	//un utente può visualizzare un pacchetto
	visualizza: set Pacchetto
}

//classe Impiegato specializzazione della classe astratta Utente
sig Impiegato extends Utente{	

	//un impiegato puà creare, modificare o eliminare un pacchetto
	creaPacchetto: set Pacchetto,
	modificaPacchetto: set Pacchetto,
	eliminaPacchetto: set Pacchetto
}

//classe Cliente specializzazione della classe astratta Utente
sig Cliente extends Utente{

	//un cliente può selezionare uno o più pacchetti
	seleziona: set Pacchetto,
	//un cliente può modificare o acquistare un istanza del pacchetto
	modificaIstanzaPacchetto: set IstanzaPacchetto,
	acquista: set IstanzaPacchetto,
	//un cliente può invitare uno o più amici
	invita: set Amico
}

//classe Amministratore specializzazione della classe impiegato
sig Amministratore extends Impiegato{
	
	//un amministratore può creare un profilo impiegato
	creaImpiegato: set Impiegato,
	
	//un amministratore può eliminare un profilo cliente o impiegato
	eliminaUtente: set Utente
/*	eliminaCliente: set Cliente,
	eliminaImpiegato: set Impiegato*/
}

//classe Amico
sig Amico{

	//utente seleziona un pacchetto, e quindi crea un' istanza del pacchetto. Utente invita degli amici a visualizzare tale istanza. Tali amici quindi condividono quest' istanza
	condivide: some IstanzaPacchetto
}

//classe Pacchetto
sig Pacchetto{
	//ad un pacchetto possono essere associate una o più istante
	selezionato: set IstanzaPacchetto
}

//classe IstanzaPacchetto
sig IstanzaPacchetto{

	//ad ongi pacchetto è assegnato un ID
	identificativo: one ID,
}


sig Username{}  //classe Username
sig Password {} //classe Password
sig ID{}              //classe ID


// VINCOLI
fact {

//VINCOLI SULL' AMMINISTRATORE
	// nel sistema deve essere presente uno ed un solo amministratore 
	one Amministratore  

//VINCOLI SUGLI ATTRIBUTI
	//due utenti non possono avere lo stesso username
	no u1, u2: Utente | u1!=u2 and u1.username=u2.username 
	
	//username, password e ID non esistono se non associati ad un utente:
	all p:Password | some u: Utente | p in u.password
	all usr: Username | some u: Utente | usr in u.username
	all id: ID | some ip: IstanzaPacchetto | id in ip.identificativo

	// non possono esistere due istanze pacchetto con lo stesso ID
	no ip1, ip2: IstanzaPacchetto | ip1!=ip2 and ip1.identificativo=ip2.identificativo


//VINCOLI SULL' UTENTE
	//un utente può essere eliminato una sola volta
	//in particolare l' amministratore non può eliminare se stesso
	no a: Amministratore, u1, u2: Utente | u1=u2 and (u1+u2) in a.eliminaUtente


//VINCOLI SULL' IMPIEGATO	
	//un impiegato non esiste se non creato dall' amministratore
	all i: Impiegato  | one a:Amministratore|  i in a.creaImpiegato


//VINCOLI SULL AMICO
	// Un amico non esiste se non invitato da un cliente
	all a:Amico  | some c: Cliente | a in c.invita and (a.condivide in c.seleziona.selezionato) 
	//ad ogni amico invitato da un cliente, deve corrispondere un pacchetto per il quale l' amico è stati invitato
	//dal punto di vista logico: preso un amico,se utente è in relazione con amico allora amico è in relazione con istanzapachetto
	all a:Amico | #invita.a=#a.condivide

//VINCOLI SUL PACCHETTO
	//Un pacchetto esiste solo se creato da un impiegato
	all p: Pacchetto | one i: Impiegato | p in i.creaPacchetto
	//un pacchetto può essere eliminato una sola volta
	all p: Pacchetto | #eliminaPacchetto.p<=1


//VINCOLI SULLE ISTANZE DEI PACCHETTI
	//una istanza non esiste se il relativo pacchetto non è stato selezionato da almeno un cliente
	all ip: IstanzaPacchetto | one p: Pacchetto | (ip in p.selezionato)
	//se un pacchetto è stato selezionato da almeno un cliente, allora ha almeno un' istanza
	all c: Cliente, p: Pacchetto | p in c.seleziona implies #p.selezionato>=1
	//un pacchetto ha un numero di istanze pari al numero di clienti che l' hanno selezionato
	all p: Pacchetto | #seleziona.p=#p.selezionato

	//se un' istanza è stata modifica dal cliente, allora il relativo pacchetto deve essere stato selezionato dal tale cliente
	all c: Cliente, ip: IstanzaPacchetto | ip in c.modificaIstanzaPacchetto implies ip in c.seleziona.selezionato
	//se un' istanza è stata acquistata dal cliente, allora il relativo pacchetto deve essere stato selezionato dal tale cliente
	all c: Cliente, ip: IstanzaPacchetto | ip in c.acquista implies ip in c.seleziona.selezionato
}

//PREDICATI

//Predicato per la creazione di un nuovo impiegato
//Viene verificato che la creazione di un nuovo impiegato non renda il sistema inconsistente
pred addImpiegato(aNew, aOld: Amministratore, i: Impiegato) {
	aNew.creaImpiegato=aOld.creaImpiegato + i
}

pred showAddImpiegato(aNew, aOld: Amministratore, i: Impiegato) {
	
	addImpiegato[aNew, aOld,i]
	#aNew.creaImpiegato=#aOld.creaImpiegato + 1
}




//ASSERZIONI

//Verifichiamo se lo stesso impiegato viene eliminato due volte
//Grazie al controesempio trovato, ci siamo accorti che l' amministratore poteva eliminare anche se stesso, cosa che non vogliamo che accada
//Abbiamo quindi inserito un altro constrain per evitare questo
assert ImpiegatoEliminato{

	no a: Amministratore, i1, i2: Impiegato | i1=i2 and (i1+i2) in a.eliminaUtente
}

//dopo aver inserito il giusto vincolo, non vengono trovati più controesempi
//check ImpiegatoEliminato



pred show () {
//POSSIAMO VINCOLARE IL NUMERO DI ISTANZE PRESENTI NEL SISTEMA
/*
    #Impiegato=2
	#Cliente=2
	#Amico=2
    #Pacchetto=2
    #IstanzaPacchetto=2
*/
}
//POSSIAMO DEFINIRE IL NUMERO MASSIMO DI ENTITA' PRESENTI NEL SISTEMA
run show // for 3 Utente, 2 Pacchetto, 1 Amico, 2 IstanzaPacchetto, 3 Username, 3 Password, 2 ID

